$\forall$${\it es}$:ES, $e$, ${\it e'}$:E. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ pred($e$) $\leq$loc ${\it e'}$  $\Rightarrow$ (${\it e'}$ $<$loc $e$) $\Rightarrow$ (${\it e'}$ = pred($e$))